| Definitions | False, True, tt, with declarations ds:dsda:dak(v) sends f s v on link l, suptype(S; T), Valtype(da;k), S  T, SQType(T), P   Q, P  Q, A c B, State(ds), z != f(x) P(a;z), M.state, P  Q, Top, a in dom(M.pre), Y, ff, reduce(f;k;as), deq-member(eq;x;L), M.rframe(A.sends tfL of k on l), M.bframe(k sends on l), M.sframe(k sends <l,tg>), M.rframe(A.effect f of k on y), M.aframe(k affects x), M.frame(k affects x), M.rframe(A.pre p for a), ma-prob(M;b), M.da(a), b  dom(M.prob), ma-prob-da-dom(M;b), f(x), x dom(f), ma-frame-compat(A;B), ma-prob-da(M), Dec(P), t.2,  , mk-ma, t.1,  xdom(f). v=f(x) P(x;v), f(x)?z,  b, P & Q, Feasible(M), if b then t else f fi , only members of L read x, k sends only on links in L, k affects only members of L, (precondition a:Outcome(p) is P:State(ds) -> Bool), x : v, with declarations ds:dsda:daeffect of k(v) is x := f s v, only L sends on (l with tg), only members of L affect x :t, x : t initially x = v, R-base-ma(R), R-loc(R), @i: A, case(R)Rnone: noneleft  right: comb(left;right)base(b). base(b), t T,   x. t(x), {T}, DeclaredType(ds;x), Knd,  , [[R]], P Q, x:A. B(x),  A, Unit,  , Normal(ds), Normal(T), x(s), R-Feasible(R),  , Dsys, State(ds) |
| Lemmas | map wf, l member wf, IdLnk sq, fpf-ap wf, tagof wf, lnk-decl-dom-implies, lnk-decl-ap, fpf-join-dom, fpf-join-ap-sq, lnk-decl-cap, assert of bnot, eqff to assert, bnot wf, iff transitivity, assert-eq-lnk, eqtt to assert, rcv wf, lnk-decl wf, fpf-join-cap-sq, fpf-cap-single-join, ma-single-sends wf, R-interface, R-compat-implies, m-sys-feasible-join, R-Dsys-Rplus, Rrframe wf, ma-single-rframe wf, Rbframe wf, ma-single-bframe wf, Raframe wf, ma-single-aframe wf, finite-prob-space wf, Rpre wf, p-outcome wf, decidable p-outcome, assert-eq-knd, locl wf, bool wf, ma-single-pre wf, fpf wf, decl-state wf, Reffect wf, decl-type wf, pi2 wf, pi1 wf, deq wf, product-deq wf, not wf, Knd sq, fpf-trivial-subtype-top, ma-state wf, ma-valtype wf, fpf-cap wf, Kind-deq wf, fpf-cap-single1, subtype rel self, fpf-single wf3, ma-single-effect wf, Rsframe wf, ma-single-sframe wf, lsrc wf, Rframe wf, ma-single-frame wf, Id wf, rationals wf, Rinit wf, int inc rationals, Knd wf, IdLnk wf, false wf, top wf, fpf-single wf, fpf-dom wf, assert wf, Id sq, id-deq wf, fpf-single-dom, ma-single-init wf, m-sys-at-feasible, Rnone wf, d-feasible-null, es realizer wf, R-Dsys wf, d-feasible wf, R-Feasible wf, es realizer-induction |